c formula generated with seed 7, probabilty values 0.414000 0.028000 0.503000 and clause ration 4.408889
c the planted solution is {1, 2, 3, 7, 8, 9, 10, 12, 15, 16, 18, 19, 21, 23, 24, 25, 26, 28, 30, 32, 33, 34, 36, 38, 39, 40, 42, 45, 46, 48, 49, 51, 54, 55, 56, 58, 61, 62, 64, 65, 66, 68, 69, 70, 71, 73, 76, 77, 79, 83, 87, 90, 92, 95, 98, 101, 102, 103, 104, 108, 109, 112, 114, 115, 117, 118, 124, 125, 126, 128, 129, 131, 132, 133, 135, 136, 137, 143, 144, 145, 149, 152, 154, 155, 156, 164, 165, 167, 168, 170, 171, 173, 175, 176, 177, 181, 182, 183, 186, 188, 190, 191, 192, 193, 195, 198, 203, 204, 207, 208, 210, 214, 216, 217, 220, 230, 231, 232, 233, 239, 241, 243, 247, 248, 249, 250, 253, 254, 255, 257, 258, 260, 261, 262, 263, 266, 267, 268, 270, 273, 277, 278, 279, 284, 285, 286, 287, 288, 291, 292, 294, 299, 300, 302, 303, 304, 305, 306, 307, 309, 310, 311, 312, 313, 314, 315, 317, 319, 320, 321, 322, 326, 328, 331, 332, 333, 336, 337, 338, 343, 345, 350, 351, 354, 358, 359, 364, 365, 369, 372, 375, 376, 377, 378, 380, 385, 387, 390, 392, 394, 396, 397, 402, 406, 407, 409, 412, 413, 414, 415, 418, 420, 421, 422, 423, 424, 425, 427, 428, 431, 432, 433, 435, 437, 438, 440, 441, 442, 443, 448, 449, 450}
p cnf 450 1984
-387 288 -117 0
79 -242 -138 0
-340 -333 -104 0
-331 163 3 0
210 -115 -359 0
-326 433 447 0
94 201 198 0
-251 -324 -229 0
245 82 -44 0
288 -29 -222 0
181 -115 401 0
-290 -146 -274 0
107 -323 334 0
-30 -426 404 0
-329 334 -252 0
189 -314 -356 0
1 236 110 0
374 -263 317 0
-9 200 -329 0
157 -436 159 0
-361 171 -219 0
-195 -389 -249 0
-200 -66 4 0
-321 -391 244 0
37 -170 -187 0
-380 -167 309 0
-367 -211 -361 0
398 73 -193 0
-35 38 195 0
-245 156 390 0
60 137 248 0
-63 279 -213 0
-298 -17 -93 0
167 -369 -307 0
-297 248 -160 0
-79 2 172 0
113 328 -87 0
284 189 256 0
344 250 400 0
314 -11 145 0
-108 75 -356 0
319 37 96 0
119 156 -3 0
305 -300 -230 0
-298 333 -174 0
-409 134 181 0
-210 -23 233 0
-206 -324 -235 0
-445 -287 223 0
-412 -339 271 0
-6 84 -124 0
-320 298 243 0
158 -293 80 0
343 230 284 0
141 -423 -340 0
-223 -81 165 0
61 -113 -27 0
-1 -45 -158 0
292 -315 209 0
-258 78 -44 0
370 421 389 0
170 139 13 0
-266 -43 -425 0
436 -77 62 0
-382 287 -410 0
-389 29 189 0
-433 370 -197 0
-236 339 -387 0
180 -141 341 0
-395 327 265 0
250 -431 -425 0
-258 65 -165 0
-233 345 151 0
-384 -315 252 0
227 -425 -400 0
396 240 408 0
-99 -208 35 0
5 -223 134 0
-134 -289 -75 0
-244 -232 -18 0
-53 -255 403 0
-91 285 -41 0
343 -191 17 0
127 385 -396 0
425 -346 -388 0
-369 -196 -336 0
274 -154 365 0
-212 395 -364 0
-326 301 207 0
-327 190 -224 0
174 330 254 0
-53 -119 -323 0
358 216 128 0
-95 -436 -323 0
-155 41 -151 0
-412 -119 157 0
156 370 237 0
-38 -428 182 0
60 439 -163 0
-145 23 -307 0
5 291 419 0
-48 439 98 0
429 112 -177 0
122 -418 310 0
111 -353 399 0
-448 -144 328 0
76 41 107 0
309 -143 148 0
-37 303 -246 0
-446 -244 -113 0
-278 -302 -174 0
177 385 -91 0
-291 26 -322 0
251 -83 -301 0
23 421 30 0
-423 203 447 0
-400 -106 -298 0
-262 -355 -409 0
345 181 -57 0
242 -78 226 0
48 -141 -6 0
62 38 -57 0
-72 402 155 0
-229 195 186 0
182 68 -100 0
-330 -414 -129 0
-113 -170 -34 0
8 -400 -14 0
-14 216 262 0
347 118 100 0
-158 372 359 0
48 58 -88 0
73 -343 329 0
89 336 -305 0
-61 -261 232 0
-206 -314 -29 0
104 69 333 0
243 301 395 0
-23 -317 -74 0
-93 402 -297 0
119 78 375 0
275 -285 -72 0
-234 -414 -145 0
12 381 194 0
-225 272 411 0
-382 -193 31 0
283 76 -144 0
-236 -209 -130 0
-2 -72 -136 0
-66 439 190 0
271 148 -346 0
-367 58 -151 0
192 -173 280 0
-260 291 -90 0
-91 175 108 0
268 322 -417 0
101 -403 427 0
6 330 -142 0
-243 325 -357 0
-128 244 -410 0
-314 427 185 0
268 -347 -204 0
10 177 -246 0
96 240 -52 0
-318 188 -395 0
-299 -43 -195 0
-47 246 57 0
-411 -295 -47 0
-281 159 297 0
304 60 293 0
-431 25 93 0
-139 -388 -219 0
-399 -196 70 0
408 259 176 0
101 -339 277 0
-27 127 158 0
382 -383 246 0
361 42 -385 0
-309 345 -321 0
-421 353 -388 0
-193 -174 272 0
-244 91 -328 0
-377 29 -82 0
345 -354 -71 0
-288 -12 176 0
159 -222 -54 0
395 247 184 0
-313 -199 -118 0
223 -27 -267 0
307 -44 249 0
-91 -316 247 0
-341 378 -345 0
-129 -234 382 0
3 316 -19 0
25 302 -236 0
-214 205 33 0
314 122 174 0
117 -230 -32 0
-221 2 291 0
-228 -73 -188 0
-124 422 -20 0
-346 -296 12 0
-396 -414 -196 0
9 188 302 0
-162 -85 -357 0
206 -31 -438 0
-289 352 382 0
103 375 156 0
176 -445 171 0
47 -337 69 0
96 380 -435 0
-124 -398 289 0
34 -429 -85 0
250 313 -251 0
-84 -91 165 0
135 19 72 0
125 330 35 0
-432 255 -205 0
100 214 -299 0
-376 -117 -229 0
-275 -201 -444 0
34 -88 -224 0
-70 198 -83 0
415 -274 -178 0
168 -408 377 0
198 -337 17 0
-251 37 31 0
21 -377 97 0
334 14 -200 0
-318 45 232 0
-349 -239 94 0
-404 309 -274 0
-364 271 273 0
212 219 387 0
10 248 -148 0
-360 394 279 0
-398 34 -187 0
79 -360 -213 0
148 -11 -170 0
11 -347 298 0
129 -226 185 0
-371 -331 -216 0
-32 -348 148 0
-223 68 135 0
1 37 110 0
-342 423 376 0
-310 -372 56 0
272 253 4 0
274 -369 299 0
-342 -378 360 0
-385 381 25 0
-383 -64 -424 0
332 -328 13 0
269 435 259 0
-106 7 287 0
-286 -123 327 0
19 28 -134 0
101 179 -16 0
-329 -18 436 0
-450 -305 45 0
330 331 395 0
-417 230 128 0
111 -393 160 0
-389 344 179 0
327 -190 -31 0
-30 309 162 0
-382 177 104 0
-412 75 -384 0
-5 200 -67 0
213 8 157 0
285 -175 225 0
-6 351 -289 0
356 -330 289 0
-215 -172 -445 0
-431 -421 154 0
220 -316 421 0
260 -203 -441 0
117 -127 -194 0
-216 -139 -402 0
-383 164 -73 0
352 334 -139 0
-158 25 287 0
19 -348 -10 0
325 210 -437 0
298 177 -181 0
-370 -59 394 0
-1 -336 -201 0
312 310 98 0
-411 266 421 0
-98 -257 -373 0
396 230 437 0
-339 -335 -201 0
60 227 422 0
-396 11 177 0
217 -187 -200 0
-45 152 -19 0
11 315 386 0
-180 -217 -309 0
21 417 403 0
170 -115 -183 0
-216 -230 -67 0
104 306 288 0
338 -434 -297 0
-47 -157 -206 0
-263 170 -376 0
-160 -353 -221 0
199 210 141 0
410 -371 352 0
62 -434 -405 0
-21 -27 -351 0
-267 238 -410 0
-441 -213 41 0
35 194 64 0
416 76 159 0
-215 322 214 0
-93 -231 -62 0
-318 -69 -133 0
-254 -276 -48 0
-323 37 75 0
-244 -60 -146 0
-194 288 19 0
390 -270 274 0
43 446 -201 0
-413 -186 420 0
61 447 -165 0
-228 108 -88 0
87 103 263 0
207 -317 -315 0
-46 230 386 0
-122 366 430 0
-69 -405 -16 0
361 277 43 0
111 -410 339 0
302 -345 -277 0
-257 15 223 0
81 37 -388 0
-125 151 156 0
79 -238 377 0
331 -398 414 0
125 -235 -298 0
-163 -251 115 0
322 193 136 0
-123 142 119 0
-210 38 -133 0
-321 -277 40 0
408 434 257 0
-221 27 -54 0
-158 206 -7 0
397 -203 -106 0
-422 -62 -209 0
378 227 57 0
-174 312 214 0
137 53 -208 0
-261 -106 262 0
312 303 -178 0
203 -282 -368 0
-428 -283 -285 0
198 -371 79 0
203 248 154 0
-221 -98 137 0
276 385 -1 0
-169 -239 297 0
-152 35 175 0
202 -370 -311 0
-349 243 -411 0
307 6 -450 0
-349 270 -91 0
-241 247 -255 0
105 -33 -225 0
15 -437 269 0
-369 -361 -30 0
70 54 -127 0
-185 -408 -417 0
108 -191 226 0
309 283 1 0
-374 -237 32 0
36 -51 -425 0
146 84 -229 0
-181 -370 37 0
-210 251 9 0
197 -419 382 0
-63 -152 -32 0
-388 315 375 0
289 11 190 0
331 -397 242 0
-252 179 -49 0
440 -432 213 0
-432 336 348 0
220 448 -370 0
434 185 -85 0
292 -66 -191 0
339 157 380 0
-156 142 -434 0
-333 290 332 0
203 362 -260 0
-3 284 401 0
56 -42 107 0
147 -449 -324 0
186 -291 271 0
214 -145 -369 0
-128 248 119 0
40 -135 -193 0
398 344 -138 0
268 -353 -340 0
-284 255 -268 0
-118 -237 -10 0
192 -267 -423 0
-263 -205 -257 0
-255 -441 -205 0
-208 -398 -385 0
-447 -356 204 0
77 -223 -240 0
-417 -436 -411 0
-169 266 304 0
307 1 -94 0
314 119 206 0
431 -247 94 0
-131 -262 -41 0
-265 432 -187 0
-76 368 409 0
-96 -84 -123 0
-390 -186 414 0
296 -392 -344 0
156 95 -227 0
-269 414 56 0
-178 125 108 0
317 99 194 0
-126 67 61 0
358 234 -168 0
-359 355 -127 0
-432 212 26 0
217 -96 3 0
-289 -58 -49 0
315 -246 -187 0
112 178 298 0
365 -52 214 0
176 267 397 0
-308 220 -384 0
-248 279 -144 0
257 9 -400 0
156 391 105 0
-365 236 30 0
-93 -61 -188 0
260 -119 302 0
198 -194 -147 0
-204 -233 -11 0
-138 425 -229 0
291 -73 289 0
442 -178 -259 0
49 -30 344 0
399 200 30 0
180 121 -153 0
177 -104 -9 0
-372 250 221 0
-131 -92 320 0
38 -395 317 0
352 -294 -211 0
14 184 -334 0
-214 -218 389 0
349 -445 205 0
300 -39 -24 0
257 168 -100 0
-56 428 -25 0
220 -311 -257 0
23 -277 426 0
-62 -145 319 0
362 202 171 0
-358 -274 281 0
93 -58 69 0
195 -241 -83 0
-393 208 -341 0
-298 -334 -222 0
99 328 -315 0
-111 265 50 0
-91 -149 342 0
-331 -290 -294 0
-79 -408 148 0
27 -371 -279 0
284 14 264 0
277 -358 94 0
289 333 -318 0
413 -16 89 0
-400 97 280 0
-100 316 120 0
-293 -292 -118 0
19 -43 -150 0
8 230 68 0
-296 -226 372 0
-354 -100 -19 0
274 -432 -318 0
218 267 -108 0
-76 357 26 0
28 67 -372 0
-349 -304 293 0
351 281 -309 0
69 383 -387 0
-370 371 -441 0
-1 406 265 0
165 385 422 0
-160 -334 147 0
8 202 -423 0
170 311 77 0
-207 339 26 0
-410 -198 -441 0
-17 155 104 0
294 138 290 0
329 441 -286 0
-78 -129 393 0
256 331 -262 0
87 -262 -267 0
-293 -60 5 0
-398 -150 303 0
182 326 450 0
-314 286 -56 0
-106 225 -73 0
209 -293 348 0
347 393 -75 0
208 198 33 0
-71 338 -79 0
-111 268 278 0
167 -75 412 0
-108 -141 418 0
432 166 252 0
-276 155 -295 0
11 439 326 0
-358 248 47 0
-122 -402 436 0
-20 443 -84 0
97 -88 -73 0
422 120 373 0
295 -386 -406 0
148 -118 -205 0
-86 -168 130 0
-118 -345 387 0
374 -83 250 0
-370 441 -53 0
81 49 106 0
324 102 94 0
421 65 -288 0
-61 200 167 0
403 -306 247 0
88 -121 61 0
-229 -386 149 0
46 -29 -340 0
-431 -359 9 0
-211 -14 -329 0
177 -125 -132 0
-201 -192 -435 0
40 304 -419 0
-450 266 -137 0
-264 -360 70 0
-172 413 -352 0
-96 329 151 0
231 13 373 0
267 -406 283 0
-193 -275 -333 0
71 269 222 0
424 93 -266 0
321 24 103 0
-229 -332 221 0
48 -79 436 0
407 219 -306 0
-96 -328 77 0
-180 103 90 0
-106 377 -229 0
372 300 -130 0
386 -408 -231 0
358 -252 108 0
-432 -284 145 0
341 444 442 0
-13 -309 -192 0
-56 -300 -445 0
181 -252 -237 0
242 -302 437 0
428 268 188 0
-368 -72 331 0
287 -241 301 0
348 -159 17 0
-306 241 -414 0
-101 159 -265 0
-332 -122 398 0
252 -63 245 0
-182 376 -422 0
59 -283 -154 0
-13 -104 -424 0
143 -368 -360 0
-1 -246 -8 0
149 249 -158 0
-400 430 -76 0
294 -78 267 0
-43 -373 15 0
-211 -440 -177 0
-353 -322 -233 0
-116 -148 266 0
-185 122 252 0
260 -73 218 0
298 311 -90 0
171 67 -437 0
-172 176 -447 0
429 188 -143 0
402 301 -195 0
24 391 11 0
24 -39 -333 0
-305 428 -312 0
-332 -317 -382 0
164 -213 441 0
-109 -115 -22 0
152 -44 73 0
-203 -28 -139 0
218 -434 -300 0
434 387 -333 0
-253 -100 134 0
-431 -32 117 0
-397 10 -364 0
-116 403 4 0
-129 131 -315 0
-304 115 -277 0
-254 147 287 0
203 -126 -313 0
53 -412 448 0
-99 -86 144 0
-72 -172 -166 0
15 344 245 0
-206 -445 396 0
-317 240 -411 0
-196 -287 396 0
32 -18 212 0
3 199 -437 0
6 414 -232 0
-76 -153 225 0
248 319 -283 0
-110 -173 148 0
268 -416 -157 0
-34 97 -393 0
57 -120 -319 0
418 -137 -256 0
403 -214 233 0
294 -197 287 0
409 373 -332 0
-10 -234 185 0
-386 93 -420 0
-419 -47 -224 0
23 177 294 0
-340 278 210 0
191 -59 -382 0
-274 -291 67 0
-235 -233 234 0
-381 429 347 0
65 304 -446 0
243 10 -93 0
-359 -96 -249 0
30 146 130 0
175 425 373 0
260 -98 -30 0
161 -168 73 0
-428 163 3 0
149 -380 327 0
43 -381 -192 0
318 426 192 0
-209 -139 -140 0
394 -77 -117 0
316 329 322 0
72 450 -447 0
-299 433 -314 0
370 -127 111 0
251 -351 -107 0
116 -294 380 0
-334 -259 -318 0
3 10 128 0
-196 109 217 0
-222 -38 -326 0
-226 -20 -393 0
-279 -286 -283 0
-390 376 -79 0
416 -72 183 0
-270 -87 307 0
372 -107 152 0
-420 -156 -67 0
385 340 -217 0
346 230 -46 0
372 -189 -244 0
195 76 303 0
109 -76 -354 0
-13 370 -287 0
435 -224 396 0
445 -188 118 0
87 206 -423 0
76 269 -413 0
-438 367 230 0
313 -437 -226 0
-230 88 -43 0
-253 -367 381 0
372 151 429 0
76 -395 -59 0
415 272 -369 0
42 -260 433 0
-407 -345 -130 0
413 153 410 0
283 -144 19 0
203 62 -340 0
-220 268 -25 0
-376 60 109 0
326 131 87 0
-329 334 -384 0
227 -152 -29 0
199 221 66 0
-97 -377 -380 0
-303 231 141 0
70 104 -225 0
129 -412 -28 0
352 204 134 0
-331 -398 -249 0
-60 -74 -223 0
60 319 158 0
156 6 -131 0
-112 -105 408 0
40 -318 414 0
249 -184 -360 0
-52 -402 157 0
-249 -291 385 0
90 -172 266 0
191 136 8 0
-430 -427 352 0
-421 -291 304 0
-53 -298 375 0
-283 56 323 0
192 274 -285 0
-362 157 209 0
387 189 111 0
-110 204 427 0
-249 184 129 0
209 403 -72 0
-105 -291 -247 0
-218 227 -397 0
204 360 -98 0
-215 413 -295 0
-72 -85 -5 0
-414 324 333 0
110 328 -257 0
-347 -174 132 0
420 431 392 0
-114 103 379 0
-34 137 110 0
-235 -427 150 0
344 -202 386 0
-330 -297 -432 0
227 -364 -389 0
-438 409 13 0
-239 -271 374 0
132 167 32 0
44 -397 -327 0
84 -122 -241 0
242 -415 -389 0
67 339 128 0
319 -120 -408 0
-331 -311 -227 0
209 237 333 0
98 -162 -134 0
-64 -19 190 0
401 -411 113 0
444 -239 -205 0
-39 -245 -83 0
37 205 -446 0
434 152 -303 0
403 -332 -335 0
416 32 324 0
381 353 71 0
26 -384 19 0
-341 298 -299 0
-344 60 349 0
-285 -94 -95 0
-347 -315 -46 0
287 -18 411 0
180 79 209 0
2 -67 -184 0
-360 -383 278 0
93 268 -183 0
-144 -29 403 0
250 -308 -252 0
-403 116 -369 0
-111 167 315 0
256 362 -234 0
27 -211 330 0
-432 -27 -109 0
70 -227 394 0
-384 -219 92 0
-135 -14 29 0
-93 -363 409 0
-170 -397 -105 0
66 -93 319 0
422 -281 198 0
118 442 -157 0
337 39 -119 0
-240 358 250 0
62 -30 -309 0
-172 -211 -99 0
-115 374 -301 0
-420 73 -449 0
-177 30 446 0
-108 -134 -175 0
-401 -133 -193 0
-234 -228 390 0
313 1 -37 0
109 413 12 0
-53 60 -203 0
83 -262 341 0
-192 -177 311 0
331 226 -437 0
439 -407 260 0
-88 -271 156 0
-374 430 43 0
-447 7 21 0
-225 -215 -227 0
207 421 -162 0
-220 -120 213 0
-146 -355 8 0
-111 -172 -341 0
78 -446 -62 0
-312 138 -236 0
-72 -384 190 0
404 136 180 0
217 387 -383 0
94 -332 -391 0
271 177 82 0
-273 104 -338 0
69 151 -109 0
-362 -43 -308 0
212 400 -196 0
-239 392 -311 0
-363 151 245 0
-349 -74 -297 0
-171 37 12 0
305 -350 -103 0
-386 -107 -59 0
-67 62 -187 0
371 333 -266 0
-297 73 233 0
-145 338 -51 0
-358 331 -292 0
-118 186 121 0
364 81 -48 0
421 413 -197 0
-101 -366 158 0
-362 -156 234 0
-384 203 -242 0
293 379 315 0
144 -145 244 0
-167 313 -261 0
-268 -427 90 0
-46 120 26 0
-175 -179 -155 0
70 -210 -428 0
-22 -227 115 0
-45 283 128 0
-370 -436 303 0
-121 266 428 0
188 232 394 0
-24 -33 354 0
239 139 -173 0
124 -265 -72 0
-74 189 -117 0
-175 385 185 0
181 -130 292 0
23 419 -73 0
179 345 113 0
379 -219 -220 0
-90 -155 -382 0
-378 -12 -93 0
35 -447 -102 0
450 333 42 0
125 337 -352 0
186 -184 132 0
-46 328 -372 0
-411 -271 68 0
-116 -31 -113 0
329 -210 250 0
-441 101 116 0
432 -127 -398 0
-284 -82 335 0
-182 334 306 0
-56 170 158 0
-367 331 413 0
266 -293 -213 0
154 176 -283 0
16 32 -194 0
-180 -1 -66 0
150 -142 222 0
444 61 295 0
-138 194 -266 0
-53 80 226 0
-436 306 33 0
343 -209 -157 0
-32 73 -33 0
113 6 -282 0
162 109 408 0
-166 424 310 0
-76 -82 236 0
156 -422 -230 0
115 -437 -9 0
258 243 -116 0
-196 -238 21 0
94 -426 366 0
234 422 77 0
-263 95 -103 0
-431 -185 97 0
145 -369 5 0
222 -154 372 0
172 -197 83 0
29 -45 220 0
372 23 394 0
271 -190 392 0
-304 -132 249 0
-334 -59 351 0
-318 98 28 0
-137 4 285 0
162 43 -298 0
43 62 -432 0
75 432 235 0
-223 252 -214 0
-19 120 112 0
197 144 -338 0
6 180 71 0
188 -236 337 0
253 283 -241 0
183 -168 -314 0
-61 42 -354 0
-192 -435 104 0
414 -58 -26 0
-159 -266 -437 0
-366 -205 420 0
-294 124 327 0
-56 -308 227 0
-352 -360 414 0
165 342 35 0
422 101 -405 0
-20 -395 204 0
102 -113 -199 0
-306 -249 292 0
344 -315 287 0
146 -117 249 0
352 -232 -404 0
-184 -99 -237 0
-308 -149 -8 0
191 -244 -298 0
181 -99 118 0
119 74 -215 0
411 -108 112 0
450 230 -405 0
187 413 -71 0
-158 394 443 0
108 18 191 0
355 401 267 0
-44 -398 165 0
-43 -127 -215 0
-153 -49 -319 0
248 183 -387 0
-73 409 -208 0
-247 441 327 0
-271 136 30 0
181 335 324 0
53 110 288 0
-132 -211 -241 0
-33 193 -152 0
-214 -142 353 0
376 304 291 0
449 24 -196 0
226 -423 25 0
-308 -418 140 0
435 -193 -128 0
-111 29 -297 0
-175 -386 -126 0
-72 201 -248 0
-220 48 290 0
209 435 389 0
-226 109 33 0
-3 129 44 0
-423 309 -102 0
365 424 409 0
-193 160 54 0
-370 -405 -400 0
114 -291 -431 0
-232 -160 -19 0
-362 -8 -2 0
-185 -346 -219 0
244 -3 48 0
6 -335 -420 0
380 391 -32 0
314 -66 352 0
123 15 -95 0
344 243 -102 0
-329 -241 -190 0
-233 -162 -338 0
398 -312 -426 0
-87 186 -9 0
-221 266 -98 0
-267 21 446 0
-198 107 322 0
-147 -251 -86 0
362 -44 -371 0
-44 25 109 0
-307 -55 -265 0
-134 -54 197 0
-97 120 200 0
45 184 -171 0
-57 348 417 0
-224 -197 311 0
448 398 -56 0
250 -241 201 0
321 -237 -367 0
-449 -140 99 0
54 -88 -158 0
-28 195 -351 0
-417 -204 41 0
429 -334 -311 0
163 -394 62 0
-321 -273 -157 0
236 -420 233 0
-224 83 -146 0
71 65 92 0
-282 94 283 0
-67 425 125 0
-16 183 13 0
-222 279 257 0
-310 409 353 0
-33 -420 220 0
1 -135 88 0
242 397 -154 0
-92 206 -80 0
347 -315 -127 0
-119 329 130 0
-428 400 -127 0
-406 -34 -357 0
262 251 -307 0
398 -139 -210 0
-158 -61 -193 0
247 175 -301 0
-284 141 -225 0
164 -390 410 0
199 -102 268 0
447 164 386 0
384 397 -438 0
1 63 206 0
222 189 -86 0
-335 -5 418 0
41 -205 -443 0
76 230 -235 0
-317 369 99 0
118 41 -155 0
-415 191 -337 0
107 87 -31 0
-94 -13 377 0
-437 -427 343 0
294 28 -20 0
-407 -399 -246 0
-111 152 -271 0
397 -51 100 0
-353 -93 -447 0
325 302 -311 0
-273 184 -211 0
-119 -191 340 0
87 -20 -142 0
245 -93 327 0
404 -395 -156 0
333 70 -408 0
286 -50 182 0
144 150 330 0
-285 -292 -153 0
85 -416 417 0
-9 282 -340 0
35 218 -325 0
-349 -337 -126 0
17 346 208 0
149 97 70 0
-418 343 59 0
419 -167 328 0
-214 216 -300 0
157 -69 26 0
142 -190 -408 0
280 187 -142 0
-381 -426 -386 0
-318 -406 363 0
141 -421 -82 0
-357 229 -140 0
14 -318 324 0
-127 257 261 0
426 223 65 0
-26 435 150 0
221 125 -16 0
-39 393 286 0
-349 -236 418 0
308 -352 -152 0
293 221 438 0
-66 359 -14 0
69 -338 -253 0
314 -368 -221 0
310 68 -72 0
-64 301 -404 0
281 -178 -418 0
112 -144 -243 0
68 -81 -189 0
304 -6 442 0
-107 -54 275 0
56 -156 -305 0
-447 308 -65 0
-290 -198 -1 0
-311 -441 -134 0
-243 -211 439 0
394 358 -325 0
207 -98 335 0
-440 -73 320 0
362 -180 194 0
60 -386 -414 0
122 -284 143 0
371 -217 -206 0
-19 259 -393 0
-307 201 262 0
-196 143 299 0
-318 -89 12 0
-283 -137 38 0
-301 -86 442 0
371 93 -199 0
238 76 121 0
431 -246 166 0
-36 412 401 0
223 347 247 0
-110 -374 -256 0
265 156 94 0
-282 325 27 0
-172 -27 442 0
175 -208 -385 0
284 423 441 0
272 -230 -395 0
267 117 -63 0
18 95 -146 0
-22 -81 365 0
155 362 -250 0
-408 342 -62 0
220 78 -354 0
158 285 -200 0
-290 -274 176 0
-327 82 -332 0
-171 -198 -381 0
-143 -296 329 0
-145 449 356 0
431 189 316 0
214 -159 109 0
-232 -155 433 0
406 -184 191 0
-130 -354 -118 0
-227 334 395 0
317 -222 -246 0
329 344 345 0
430 50 406 0
187 -217 -404 0
241 -332 344 0
355 -278 -50 0
-113 -178 267 0
-46 -313 -357 0
-103 383 376 0
3 -87 275 0
108 -132 -145 0
-163 408 381 0
54 149 337 0
-243 370 39 0
170 331 -64 0
-441 -99 29 0
431 -211 198 0
-190 116 365 0
414 -421 106 0
-149 408 255 0
-56 -374 -2 0
120 -10 -179 0
-263 422 172 0
407 151 379 0
-441 134 277 0
174 165 -18 0
421 198 300 0
-214 -80 -392 0
270 240 -449 0
-36 92 283 0
203 -309 -210 0
353 387 330 0
-89 -11 -179 0
-363 -357 -200 0
113 168 257 0
-449 -191 -360 0
275 317 217 0
291 88 395 0
-38 -211 14 0
111 360 338 0
-344 -416 107 0
407 -103 -208 0
175 223 -83 0
385 16 302 0
347 -269 367 0
9 128 -6 0
-230 183 237 0
-415 323 -140 0
-62 -167 -29 0
268 50 -202 0
-380 431 -208 0
-400 -206 216 0
-262 -77 407 0
156 -178 126 0
-198 -410 -232 0
117 300 351 0
150 -30 -327 0
236 208 -1 0
-449 -337 309 0
-347 390 -339 0
294 165 385 0
-116 -95 -287 0
447 -392 -352 0
190 -186 6 0
-269 397 -235 0
22 6 -140 0
220 370 180 0
187 -143 -238 0
4 331 316 0
-245 268 -405 0
261 -149 17 0
-300 -97 -9 0
20 -195 -106 0
-424 -297 -377 0
434 -362 -443 0
88 -267 167 0
87 358 -400 0
172 242 302 0
-426 429 83 0
-141 369 -86 0
295 -360 -412 0
327 -72 120 0
-82 -74 142 0
377 447 348 0
221 -388 -443 0
-149 -108 -341 0
-150 42 338 0
-189 41 -143 0
-128 62 426 0
330 -49 406 0
226 193 -417 0
304 372 402 0
-214 -392 -352 0
259 1 -216 0
-43 -34 107 0
-188 167 -128 0
-256 -398 380 0
232 -51 -38 0
220 203 190 0
436 -111 82 0
-177 10 196 0
392 -372 196 0
-29 137 220 0
146 353 143 0
275 308 165 0
-220 -149 104 0
-53 -179 -327 0
244 -240 107 0
212 128 -129 0
81 401 101 0
-200 79 -161 0
225 196 -6 0
-345 -44 -58 0
318 20 406 0
274 167 -309 0
156 159 -83 0
-21 377 142 0
428 -410 -189 0
209 -449 -110 0
315 -384 62 0
16 244 35 0
-371 282 -394 0
27 189 287 0
243 -311 367 0
-197 -121 -426 0
240 -52 -292 0
-169 129 -134 0
-57 -62 -277 0
-210 -203 -227 0
179 -117 -205 0
428 91 -54 0
-279 -169 159 0
-420 -414 28 0
150 -42 -256 0
198 291 -318 0
-55 430 421 0
-123 -399 -403 0
-339 257 -280 0
119 -125 -244 0
-199 354 443 0
-54 -445 -409 0
361 -373 -273 0
-449 110 -105 0
-359 10 324 0
391 157 165 0
80 -254 95 0
-275 -381 -356 0
-121 271 107 0
88 218 137 0
-192 183 -336 0
-366 -106 -335 0
-220 -247 -280 0
232 -316 -403 0
157 -191 1 0
-199 -322 6 0
-447 138 197 0
352 -68 -327 0
-133 -166 97 0
-251 329 192 0
428 53 174 0
-34 -393 -112 0
-327 297 -302 0
-295 185 -313 0
-144 216 -220 0
-84 -348 -353 0
-174 305 314 0
193 38 260 0
71 301 185 0
-440 -296 236 0
16 -98 130 0
184 -27 35 0
-243 -197 -102 0
57 25 349 0
-315 395 443 0
34 174 -412 0
-320 434 137 0
-166 -43 -226 0
279 -349 -281 0
398 -296 327 0
53 374 253 0
143 55 -90 0
-196 211 60 0
-310 294 -66 0
-386 265 323 0
-18 -229 -421 0
-237 -357 261 0
-90 -233 -269 0
83 -148 -436 0
-44 -327 24 0
-380 -218 -431 0
-280 -416 137 0
154 -14 -224 0
81 137 187 0
416 150 284 0
-194 -305 280 0
100 -144 440 0
-224 -133 48 0
399 -200 50 0
-299 336 -62 0
19 -30 -34 0
-221 -234 350 0
1 -442 -412 0
188 -374 -245 0
-10 340 -293 0
195 -16 -220 0
148 -155 248 0
112 427 -283 0
-251 288 -237 0
-153 -401 -21 0
36 -64 94 0
192 449 70 0
304 217 -316 0
-73 247 97 0
61 -338 -9 0
263 -356 46 0
217 357 -320 0
-73 347 -283 0
-412 422 122 0
-121 10 -166 0
-227 77 -381 0
-25 -413 -339 0
119 306 -292 0
-136 196 176 0
264 40 -320 0
290 255 426 0
-262 71 246 0
-34 -338 -134 0
135 -178 -29 0
-100 -259 233 0
-53 389 50 0
-138 358 -72 0
444 -388 96 0
-191 -424 -295 0
-207 2 -311 0
-16 -125 -225 0
167 313 311 0
438 449 450 0
-8 -73 279 0
327 -262 326 0
-292 -146 379 0
26 79 40 0
61 105 -437 0
150 16 213 0
2 322 192 0
250 353 -421 0
-315 387 -309 0
-227 -389 420 0
372 34 -224 0
102 -13 422 0
445 -199 -425 0
108 -382 67 0
-44 -100 285 0
348 131 -424 0
-240 263 65 0
43 271 -395 0
-333 -48 437 0
73 311 -399 0
-269 119 -438 0
194 -432 34 0
-394 424 -87 0
111 294 139 0
-337 157 136 0
-435 -263 204 0
-209 302 -216 0
-237 -48 -422 0
94 148 -252 0
-205 -132 -378 0
-439 312 3 0
311 -229 279 0
226 25 -321 0
198 -59 216 0
-134 125 220 0
202 -312 137 0
-79 -324 -149 0
366 210 237 0
38 -373 266 0
-11 -229 300 0
-393 68 415 0
428 177 -404 0
301 -282 -191 0
370 394 116 0
-378 170 81 0
-441 233 395 0
231 -346 241 0
40 -379 -174 0
222 77 -156 0
-221 -21 -377 0
-399 260 241 0
334 -414 -206 0
175 328 16 0
-257 39 86 0
-46 -427 -194 0
172 -189 -412 0
-12 -121 -133 0
200 -401 -87 0
-47 -194 -265 0
53 317 268 0
154 260 160 0
335 -271 -23 0
-103 58 85 0
-362 10 437 0
424 -262 60 0
-245 -203 38 0
-182 161 -283 0
14 194 49 0
-443 -309 365 0
-351 -20 94 0
-298 -8 -273 0
97 -219 229 0
-99 137 -97 0
38 -344 268 0
129 -185 168 0
-258 -449 210 0
207 179 96 0
406 -45 153 0
314 -140 -153 0
51 142 383 0
154 423 244 0
22 17 40 0
302 338 365 0
-137 -323 -204 0
243 -234 322 0
428 -218 122 0
376 30 -399 0
302 235 -190 0
89 284 -1 0
356 449 174 0
-427 86 277 0
159 -293 245 0
-11 -308 337 0
319 -246 192 0
-382 311 -81 0
-266 -125 433 0
-375 -355 -425 0
-239 -6 121 0
-3 -432 364 0
235 -293 125 0
269 -383 -48 0
-384 40 -282 0
134 237 248 0
69 302 -157 0
-213 300 -59 0
-188 250 34 0
-295 -156 391 0
-16 55 31 0
-112 284 367 0
-380 -345 450 0
44 -110 -390 0
286 80 -448 0
-386 175 21 0
212 433 293 0
321 -159 -191 0
-366 -446 443 0
410 181 -420 0
186 -381 95 0
314 397 251 0
-240 -316 449 0
273 -299 -311 0
-291 49 -328 0
273 -297 -295 0
326 -61 -214 0
419 -241 -346 0
-79 -120 -407 0
-331 156 424 0
-222 -429 177 0
-62 19 224 0
186 315 144 0
426 46 -230 0
276 13 192 0
370 219 372 0
-156 -27 -24 0
-291 -440 -6 0
324 -157 -170 0
413 287 135 0
-64 -136 -20 0
-397 312 50 0
-295 -316 -347 0
15 208 310 0
100 -154 -341 0
-341 -448 392 0
-128 -37 -90 0
-251 -385 15 0
-441 -273 -281 0
79 -119 -325 0
435 139 368 0
-22 213 399 0
-368 -50 -316 0
179 156 -317 0
25 308 -3 0
-232 168 74 0
-121 234 366 0
218 354 -250 0
1 -230 275 0
403 -226 -262 0
360 -159 -181 0
365 -317 296 0
95 -123 -185 0
259 -142 -422 0
75 100 83 0
125 -39 -62 0
38 -115 -422 0
-165 -353 -171 0
398 274 243 0
-248 6 254 0
-397 -104 230 0
-22 325 -428 0
89 82 -120 0
334 379 39 0
283 -418 -218 0
404 243 362 0
-298 -442 -226 0
-189 395 -25 0
-212 -47 239 0
79 -170 153 0
-346 407 177 0
2 -171 367 0
128 -243 416 0
136 -170 179 0
21 -434 7 0
-13 313 -324 0
-40 -281 316 0
223 -400 205 0
-224 245 -424 0
214 -373 220 0
-422 -388 -51 0
244 -361 -311 0
-350 -301 189 0
-159 -86 437 0
20 -224 -182 0
443 -3 -30 0
-420 397 -175 0
208 -94 -60 0
103 -183 -424 0
162 -161 119 0
42 441 135 0
-317 88 102 0
-444 -387 -164 0
-217 268 226 0
275 -179 -231 0
193 -345 -284 0
-308 -239 -12 0
-86 -88 195 0
-293 169 228 0
-230 36 201 0
59 426 331 0
166 -78 197 0
-414 1 13 0
151 -311 440 0
340 -216 424 0
133 19 65 0
122 172 253 0
223 279 318 0
-358 263 201 0
-389 177 -403 0
124 24 -57 0
-223 349 281 0
375 -23 142 0
-352 421 45 0
-256 309 -160 0
170 4 -406 0
-200 103 62 0
319 -34 160 0
-225 -119 9 0
434 -35 94 0
-170 189 -199 0
360 169 217 0
208 399 213 0
-298 -348 424 0
413 -303 -305 0
-308 97 142 0
265 -44 339 0
406 -289 -139 0
33 71 -323 0
149 253 -98 0
242 -137 7 0
281 226 -22 0
55 35 -376 0
-59 -43 -27 0
10 -389 207 0
-182 118 -46 0
39 250 95 0
-73 50 92 0
414 126 -366 0
-75 254 -94 0
374 -21 -81 0
-82 -246 128 0
-13 -130 146 0
344 366 309 0
-98 -416 342 0
440 -65 -435 0
-195 -235 252 0
178 333 223 0
209 -89 -186 0
167 -353 125 0
-151 2 130 0
-40 -28 332 0
191 -247 401 0
-257 -29 -319 0
-139 26 -106 0
311 51 -93 0
-216 43 -356 0
-146 281 174 0
-68 334 124 0
-420 214 -332 0
326 -1 -32 0
-228 -330 -85 0
408 -20 -1 0
120 263 318 0
220 -66 -257 0
28 -266 -198 0
-85 158 -65 0
421 213 252 0
-291 94 -417 0
-162 -202 68 0
-243 -253 -161 0
-119 -365 74 0
86 -388 398 0
192 -234 247 0
69 422 -404 0
-389 177 195 0
-316 67 -260 0
-416 414 61 0
-127 -360 -150 0
12 -7 -20 0
340 38 -438 0
302 221 89 0
-334 161 229 0
327 -406 216 0
197 60 273 0
-302 -67 -3 0
383 423 168 0
-83 438 259 0
420 -403 154 0
413 144 -324 0
60 416 10 0
-431 222 144 0
-102 380 398 0
160 346 -400 0
28 321 135 0
-342 -167 153 0
251 -150 -92 0
-224 -50 21 0
131 -262 80 0
320 -93 365 0
306 -148 200 0
-52 389 280 0
369 250 79 0
-413 119 -242 0
363 -330 119 0
137 -265 -53 0
-138 -226 239 0
-373 -340 109 0
169 7 275 0
374 -366 -48 0
-60 344 397 0
383 -14 29 0
-298 253 -224 0
-116 30 -340 0
316 268 395 0
-54 -81 439 0
-31 2 438 0
-290 282 444 0
-444 -384 -401 0
-415 343 416 0
-275 186 -251 0
172 -309 233 0
-395 416 -145 0
102 217 285 0
-233 381 51 0
214 397 350 0
387 13 -394 0
279 -394 361 0
34 -397 10 0
-355 263 -344 0
-81 -336 -415 0
-226 238 293 0
383 -338 -142 0
230 267 30 0
-248 12 -450 0
-296 139 403 0
-287 206 260 0
309 -379 144 0
111 -67 119 0
-401 407 414 0
386 -312 217 0
-228 415 69 0
405 237 -53 0
228 30 -92 0
272 -191 168 0
-220 -168 -408 0
290 -108 -344 0
144 184 -253 0
-6 256 -369 0
-106 262 -184 0
-356 -293 136 0
332 231 -264 0
-59 -36 -90 0
-101 339 232 0
-245 -258 -338 0
395 -31 107 0
-311 -63 169 0
-79 -136 248 0
-54 317 -369 0
-146 39 378 0
-364 -291 -202 0
217 -219 -430 0
3 210 300 0
-16 25 -257 0
220 -16 75 0
-283 36 -353 0
128 115 319 0
-282 -107 -246 0
-87 96 254 0
24 219 199 0
-360 22 -135 0
-61 187 312 0
-172 429 134 0
-374 228 363 0
280 -11 -198 0
-407 105 154 0
131 146 366 0
-216 -357 -83 0
191 -439 239 0
18 347 -186 0
-334 226 -361 0
-6 208 319 0
-420 166 299 0
33 -253 22 0
397 245 -230 0
172 -22 371 0
155 252 445 0
283 275 321 0
218 -87 248 0
375 35 -51 0
-59 -33 81 0
-34 -67 196 0
58 47 -306 0
215 -103 155 0
194 204 196 0
343 336 -91 0
255 385 -235 0
124 -388 -293 0
-227 -179 257 0
-241 287 236 0
448 -196 249 0
180 28 -68 0
172 102 -124 0
17 -202 -433 0
-396 -34 -426 0
-366 357 334 0
-86 283 -61 0
77 442 263 0
-282 -434 413 0
-374 -215 -341 0
358 -189 55 0
317 -295 -380 0
384 -183 -226 0
133 151 -176 0
354 -106 -6 0
166 33 -333 0
142 113 253 0
6 -310 -22 0
402 396 350 0
295 -151 74 0
370 -435 254 0
431 44 -406 0
114 69 291 0
353 -216 285 0
84 9 327 0
329 419 30 0
186 -429 -381 0
-446 -49 -303 0
446 158 131 0
178 -81 -262 0
-228 378 233 0
366 -22 228 0
449 266 32 0
104 36 -67 0
205 87 -440 0
379 359 399 0
-287 15 209 0
-135 14 98 0
-370 -105 -196 0
147 -229 398 0
209 299 139 0
-425 -408 162 0
-369 163 303 0
341 -95 350 0
414 292 214 0
-442 325 -316 0
-9 64 298 0
-261 91 428 0
-443 63 220 0
420 -324 -295 0
-172 147 -14 0
305 227 -10 0
-255 283 104 0
-198 -288 294 0
-152 132 400 0
-381 317 375 0
377 219 37 0
-61 -107 -249 0
-50 -303 403 0
-101 -11 -255 0
-320 -175 152 0
396 378 -199 0
401 -224 -300 0
77 -76 373 0
-445 247 275 0
-67 -412 -77 0
396 -259 108 0
-283 365 -221 0
79 104 108 0
366 192 -421 0
-18 199 -325 0
-409 239 -36 0
39 442 -43 0
278 -120 -346 0
-170 298 270 0
-215 -358 106 0
-266 51 -433 0
-254 19 153 0
-122 -368 -35 0
-287 -276 -378 0
165 -301 305 0
327 -56 -271 0
-236 -197 131 0
310 -25 335 0
15 94 197 0
23 -213 448 0
-293 172 175 0
342 -290 -251 0
-280 -352 285 0
-381 101 443 0
390 43 94 0
415 177 171 0
-361 431 375 0
221 66 -3 0
-333 -140 119 0
-37 448 -228 0
-77 321 -117 0
78 -330 -420 0
228 -444 -345 0
-163 197 -19 0
142 -399 318 0
-437 258 256 0
306 38 -82 0
42 -401 -91 0
252 85 -245 0
-405 -195 -294 0
-106 267 270 0
-233 -43 22 0
321 205 -144 0
-195 385 325 0
-426 -157 435 0
280 351 -302 0
399 391 412 0
84 75 -113 0
-20 -84 220 0
-445 -437 -165 0
-403 -368 438 0
-253 417 249 0
153 -341 -279 0
301 -393 -145 0
-280 -213 -374 0
-302 447 -116 0
-80 -391 -213 0
96 386 154 0
261 -126 100 0
108 -151 -184 0
365 235 265 0
-36 -320 437 0
-42 427 447 0
-155 -241 10 0
-120 -71 -1 0
-144 -211 -258 0
30 -88 424 0
193 128 -41 0
147 26 401 0
-294 360 38 0
431 -402 271 0
-367 -170 -431 0
-91 -211 -295 0
189 -281 -203 0
-62 -104 -348 0
158 -232 208 0
222 45 434 0
-140 398 31 0
173 448 314 0
-32 -327 398 0
116 374 -99 0
13 -143 38 0
-411 50 383 0
325 38 147 0
-50 -19 -1 0
-214 -123 218 0
-244 160 -432 0
40 264 -247 0
-445 -365 439 0
-141 -213 181 0
-266 -383 -155 0
447 327 190 0
73 -81 -206 0
419 -434 398 0
170 -186 403 0
-59 -368 284 0
-363 340 -424 0
118 22 147 0
335 402 123 0
331 250 312 0
32 -400 -138 0
-213 -355 392 0
-141 381 -204 0
-362 -28 245 0
-124 444 406 0
236 443 -418 0
-298 -204 180 0
-441 95 -133 0
11 210 246 0
-151 348 -214 0
-72 420 170 0
281 4 -327 0
311 63 -137 0
-291 347 247 0
288 -109 20 0
-37 -212 -14 0
293 -332 164 0
276 -201 -345 0
-371 -332 -243 0
-224 -404 -382 0
6 -202 -304 0
-427 -391 -181 0
-338 -241 76 0
10 -145 166 0